Remove Character.toChars, highSurrogate, lowSurrogate models #4534
Conversation
smowton
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d5795b5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108337049
| public class C { | ||
|
|
||
| public void test() { | ||
| char[] c = Character.toChars(5); |
| --function C.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` | ||
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| ^VERIFICATION SUCCESSFUL$ |
There was a problem hiding this comment.
Test will pass even if toChars is not implemented. because unreachable evaluates to true. Could we add an assertion that we expect to fail?
|
I think we could even remove the whole character preprocessing now that we have a model for it (it would better to have tests for it though). |
smowton
force-pushed
the
smowton/fix/character-tochars
branch
from
d5795b5 to
c725551
Compare
|
@allredj changes applied |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c725551).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108385615
Character.toChars was malformed (it tried to address a java::array[char] * like it was a raw char[], and tried to return an if_exprt of two arrays of differing type), and there is already an implementation in the models library with a perfectly good implementation. Character.highSurrogate and lowSurrogate were type unsound (creating additions of mixed type). Again, they add nothing on top of the shipped models library.
smowton
force-pushed
the
smowton/fix/character-tochars
branch
from
c725551 to
c6c9368
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c6c9368).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108541289
Character.toChars was malformed (it tried to address a java::array[char] * like it was
a raw char[], and tried to return an if_exprt of two arrays of differing type), and there
is already a perfectly good implementation in the models library.
Character.highSurrogate and lowSurrogate were type unsound (creating additions of mixed type).
Again, they add nothing on top of the shipped models library.